	//#include "test_yices.h"
#include "PDTGraphVisitor.h"
#include "PDTNumVar.h"
#include "PDTExpBoolBinNumDerived.h"
#include "PDTExpNumBinDerived.h"
#include "PDTProp.h"
#include "PDTCodeGraph.h"
#include "PDTNumConst.h"
#include <stdio.h>
#include "PDTAssign.h"
#include "PDTBoolVar.h"
#include "PDTExpBoolBinBoolDerived.h"
#include "yices_c.h"
#include "PDTIfElse.h"

#include "PDTListOfStatements.h"


int main (){
PDTCodeGraph CG;
PDTNumVar a(CG,"a");
PDTNumVar b(CG,"b");
PDTNumVar c(CG,"c");
PDTNumConstInt one(CG,1);
PDTNumConstInt three(CG,3);

PDTGreaterThan e1(CG,a,b);

PDTAdd e2(CG,b,c);
PDTAssign a2(CG,a,e2);
PDTAssign a3(CG,c,one);

vector <PDTStatement*> listIf;
listIf.push_back(&a2);
listIf.push_back(&a3);

PDTSubt e4(CG,b,c);
PDTAssign a4(CG,a,e4);
PDTAssign a5(CG,b,one);

vector <PDTStatement*> listElse;
listElse.push_back(&a4);
listElse.push_back(&a5);


PDTListOfStatements ifList(CG,listIf);
PDTListOfStatements elseList(CG,listElse);
PDTIfElse ifElse(CG,e1,ifList,elseList);

PDTAssign a6(CG,a,three);

PDTYicesVisitor gvy(CG);
PDTDefaultVisitor gvd;

ifElse.traverse(gvy);

yices_dump_context(gvy.ctx);
yices_model m;
long aa=1;
long bb=1;
long cc=1;

 switch(yices_check(gvy.ctx)) {
  case l_true:
	printf("satisfiable\n");
	m= yices_get_model(gvy.ctx);
	yices_get_int_value(m, yices_get_var_decl_from_name(gvy.ctx,gvy.constCharToChar("a")),&aa);
	yices_get_int_value(m, yices_get_var_decl_from_name(gvy.ctx,gvy.constCharToChar("b")),&bb);
	yices_get_int_value(m, yices_get_var_decl_from_name(gvy.ctx,gvy.constCharToChar("c")),&cc);

	printf("a = %ld\n",aa );
	printf("b = %ld\n",bb);
	printf("c = %ld\n",cc);
	yices_display_model(m);
	break;
  case l_false:
	printf("unsatisfiable\n");
	break;
  case l_undef:
	printf("unknown\n");
	break;
  }
  yices_del_context(gvy.ctx);

  return 0;
}
